Nuprl Lemma : deq-member_wf
0,22
postcript
pdf
A
:Type,
eq
:EqDecider(
A
),
L
:
A
List,
x
:
A
. deq-member(
eq
;
x
;
L
)
latex
Definitions
deq-member(
eq
;
x
;
L
)
,
reduce(
f
;
k
;
as
)
,
p
q
,
eqof(
d
)
,
,
false
,
EqDecider(
T
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
deq
wf
,
bfalse
wf
,
bool
wf
,
eqof
wf
,
bor
wf
,
reduce
wf
origin
A:Type, eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) 
A:Type, eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) 
qx:A. B(x) T